package simplytypedinference

/**
 * Slightly adapted from parser for untyped lambda calculus by Miles Sabin 
 */

import scala.util.parsing.input.Reader
import scala.util.parsing.combinator.lexical.StdLexical
import scala.util.parsing.combinator.syntactical.StdTokenParsers
import scala.util.parsing.combinator.ImplicitConversions


   
trait TypedLambdaParser extends StdTokenParsers  with ImplicitConversions
{
  type Tokens = StdLexical
  val lexical = new StdLexical
  lexical.reserved ++= List("unit", "let", "in", "if", "then", "else","bool","int","true", "false")
  lexical.delimiters ++= List("=>", ",",":", ".", ";", "_", "==", "(", ")", "=", "\\", "+", "-", "*", "/")


    
  def expr : Parser[LTerm] =
  ( "\\" ~ lambdas  
  | "let" ~ name ~ "=" ~ expr ~ "in" ~ expr ^^ flatten3(Let)
  | "if" ~ expr ~ "then" ~ expr ~ "else" ~ expr ^^ flatten3(If)
  | "true" ^^ Tru
  | "false" ^^ Fls
  | "unit" ^^ Unit
  | chainl1(aexpr, success(App(_: LTerm, _: LTerm)))
  )
  


  def name : Parser[Name] = "_" ^^ Name("_") | ident ^^ Name  

  def lambdas : Parser[LTerm] = 
    name ~ ":" ~ ltype ~ ("." ~ expr | lambdas) ^^ flatten3(Lam)
      
  def ltype : Parser[LType]  =
    (
    "bool" ^^ TyBool
    | "int" ^^ TyInt
    | "unit" ^^ TyUnit
  //| "(" ~ "=>" ~ "(" ~ ltype ~ "," ~ ltype ~ ")" ~")" ^^ flatten2(TyArr)
    | "(" ~ ltype ~ "=>" ~ ltype ~ ")" ^^ flatten2(TyArr)
   
    
    )
  
  def aexpr : Parser[LTerm] =
  ( numericLit ^^ (_.toInt) ^^ Lit
  | name ^^ Ref
//| "unit" ^^ Unit
  | "(" ~ expr ~ ")"
  )
  

  def parse(r: Reader[char]) : ParseResult[LTerm] =
    phrase(expr)(new lexical.Scanner(r))
}